x:chain_master(). (cmconfig?(x))  (cmconfig-list(x)  (Id List)) 

latex

Definitions	s = t, t  T, False, Id, , x:AB(x), P  Q, True, type List, chain master ind cmseq compseq tag def, b, cmconfig?(x), chain master ind cmconfig compseq tag def, x:A  B(x), left + right, chain_master(), cmconfig-list(x), x:A. B(x)
Lemmas	assert wf, cmconfig? wf, chain master wf, true wf, false wf